open cic
open shared_names
open ea

-------------------------------------------------------------------------------
-- Generic predicates
-------------------------------------------------------------------------------

pred AvailableRoles[roles: set CSR] {
	CIC.rmap[univ].role = roles
}

pred AllowedEAs[rm: DRURMapping, allowedEAs: set EA] {
	rm.unit.ea in allowedEAs	
} 

pred AvailablePorts[rm: DRURMapping, availablePorts: set EAP] {
	rm.unit.portSignatures.univ = availablePorts	
}

pred AssociateRoleWithPort[rm: DRURMapping, port: EAPL] {
	-- association means only to unify signatures
	rm.unit.portSignatures[port] = rm.signature
}

pred DelegateGlobalFeaturesToRole[rm: DRURMapping, delegatedFeatures: set FT] {
	-- all feature-values of features required by the CIC 
	-- that should be delegated are unified
	all ft: (CIC.features.univ & delegatedFeatures) {
		CIC.features[ft] = rm.unit.features[ft]		
	}
}

pred SupportedGlobalFeatures[supportedFeatures: set FT] {
	CIC.features.univ in supportedFeatures
}

pred RoleCardinalitySingle[r: CSR] {
	one rm: CIC.rmap[univ] | rm.role = r
}

pred RoleCardinalityMultiple[r: CSR] {
	some rm: CIC.rmap[univ] | rm.role = r
}

pred EmployedCA[c: CA] {
	CIC.ca = c
}

-- TODO: units are identified by their roles, what if one unit has several roles?
pred RemoteBinding[r1: CSR, p1: EAPR, r2: CSR, p2: EAPR] {
	-- there is one signature, that for both is similar for the associated
	one signature: S | all rm: CIC.rmap[univ] | {
		rm.role = r1 => rm.unit.portSignatures[p1] = signature      
		rm.role = r2 => rm.unit.portSignatures[p2] = signature      
	}	
}

-------------------------------------------------------------------------------
-- Concrete CAs
-------------------------------------------------------------------------------

-- Image of the "RPC" connector architecture
one sig CA_RPC extends CA {}
fact CA_RPC { 
	EmployedCA[CA_RPC] => {  
	
		AvailableRoles[CSR_Client + CSR_Server]
		
		RoleCardinalitySingle[CSR_Server]
		RoleCardinalityMultiple[CSR_Client]	
		
		SupportedGlobalFeatures[FT_Security]
		
		-- define implementation (EA, associated port, feature delegation) 
		-- of all supported roles
		all rm: CIC.rmap[univ] | {
			  
			-- client unit
			rm.role = CSR_Client => {
				AllowedEAs[rm, EA_RPCClientUnit + EA_InterceptedRPCClientUnit]
				
				AvailablePorts[rm, EAPLP_CallIn + EAPR_Line]
				
				AssociateRoleWithPort[rm, EAPLP_CallIn] 
			}
			-- server unit
			rm.role = CSR_Server => {
				AllowedEAs[rm, EA_RPCServerUnit]
				
				AvailablePorts[rm, EAPLR_CallOut + EAPR_Line]
				
				AssociateRoleWithPort[rm, EAPLR_CallOut]				

				DelegateGlobalFeaturesToRole[rm, FT_Security]				
			}  
		}
		
		-- port EAPR_Line of the unit implementing CSR_Client is bound to
		-- port EAPR_Line of the unit implementing CSR_Server
		RemoteBinding[CSR_Client, EAPR_Line,CSR_Server, EAPR_Line] 
		
	}
}
